Inference at * 1 2 1 
Iof proof for Lemma integer sqrt:



1. n : 
2. 0 < n
3. r : 
4. (r * r)  (n - 1)
5. (n - 1) < ((r+1) * (r+1))
  r:. (((r * r)  n) & (n < ((r+1) * (r+1)))) 

latex

 by Decide ((r+1) * (r+1))  n THEN Auto 

latex

 1: 

 1: 6. ((r+1) * (r+1))  n
 1:   r:. (((r * r)  n) & (n < ((r+1) * (r+1))))
 2: 

 2: 6. (((r+1) * (r+1))  n)
 2:   r:. (((r * r)  n) & (n < ((r+1) * (r+1))))
 .

Definitions	A  B, n * m, n+m, #$n, (xL.P(x)), xL. P(x), x f y, f(a), A c B, a < b, a <p b, a  b, a ~ b, b | a, b, Dec(P), P  Q, left + right, x:A. B(x), s = t, S  T, |g|, t  T, {x:A| B(x)} , , A, False, P  Q, x:A. B(x), P & Q, x:A  B(x), x:AB(x), Void, a < b, , n - m, -n
Lemmas	decidable le, nat wf